Nuprl Lemma : sum_unroll_base_q
11,40
postcript
pdf
i
,
j
:
. (
i
=
j
)
(
E
:({
i
..
j
}
).
i
k
<
j
.
E
(
k
) = 0
)
latex
Definitions
t
T
,
t
.2
,
t
.1
,
CRng
,
<
+*>
,
0
,
|
r
|
,
x
:
A
.
B
(
x
)
,
a
j
<
b
.
E
(
j
)
Lemmas
crng
wf
,
qrng
wf
,
rng
sum
unroll
base
origin
i, j:
. (i = j) 
(E:({i..j
}
). 
i 
k < j. E(k) = 0 
) i, j:. (i = j) (E:({i..j}). i k < j. E(k) = 0 ) T+*>x:A. B(x)a j < b. E(j)